(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 10))
(let ((e3 6))
(let ((e4 5))
(let ((e5 (- v1 v0)))
(let ((e6 (/ e4 (- e3))))
(let ((e7 (* e5 v0)))
(let ((e8 (/ e4 (- e4))))
(let ((e9 (- e5)))
(let ((e10 (+ e7 e5)))
(let ((e11 (+ e5 v1)))
(let ((e12 (- e7)))
(let ((e13 (* e10 v1)))
(let ((e14 (+ e10 e13)))
(let ((e15 (/ e3 e3)))
(let ((e16 (+ e15 e12)))
(let ((e17 (/ e3 (- e4))))
(let ((e18 (/ e3 e3)))
(let ((e19 (+ e7 e6)))
(let ((e20 (- v0 v1)))
(let ((e21 (* e17 e9)))
(let ((e22 (+ e5 e5)))
(let ((e23 (/ e3 e4)))
(let ((e24 (* e8 e22)))
(let ((e25 (* e5 v0)))
(let ((e26 (/ e4 e4)))
(let ((e27 (- e6)))
(let ((e28 (* e21 e22)))
(let ((e29 (- e18 e8)))
(let ((e30 (/ e3 (- e2))))
(let ((e31 (= e27 e9)))
(let ((e32 (= e10 e27)))
(let ((e33 (< v0 e8)))
(let ((e34 (< e16 e11)))
(let ((e35 (distinct e19 e18)))
(let ((e36 (<= e19 e5)))
(let ((e37 (= e16 e25)))
(let ((e38 (<= e6 v1)))
(let ((e39 (<= e8 e11)))
(let ((e40 (<= e24 e13)))
(let ((e41 (>= e21 v1)))
(let ((e42 (< v0 e23)))
(let ((e43 (<= e10 e5)))
(let ((e44 (> e21 e12)))
(let ((e45 (< e23 e9)))
(let ((e46 (>= e23 e17)))
(let ((e47 (> e24 e25)))
(let ((e48 (< e5 e9)))
(let ((e49 (<= e20 e29)))
(let ((e50 (< e19 e14)))
(let ((e51 (= e18 e14)))
(let ((e52 (= e20 v1)))
(let ((e53 (distinct e20 e11)))
(let ((e54 (< e20 e16)))
(let ((e55 (>= e26 e9)))
(let ((e56 (distinct e27 v1)))
(let ((e57 (<= e14 e27)))
(let ((e58 (< e27 v0)))
(let ((e59 (distinct e14 e22)))
(let ((e60 (= v1 e7)))
(let ((e61 (<= e9 e30)))
(let ((e62 (distinct e8 e8)))
(let ((e63 (= e27 v1)))
(let ((e64 (= e24 e19)))
(let ((e65 (< e26 e14)))
(let ((e66 (distinct e24 e16)))
(let ((e67 (<= e27 e9)))
(let ((e68 (>= e22 e10)))
(let ((e69 (<= e30 e25)))
(let ((e70 (<= e17 v1)))
(let ((e71 (= e9 e30)))
(let ((e72 (distinct e13 e27)))
(let ((e73 (= e13 e9)))
(let ((e74 (<= e8 e20)))
(let ((e75 (<= e9 e14)))
(let ((e76 (distinct e6 e24)))
(let ((e77 (<= e10 e15)))
(let ((e78 (> e11 e18)))
(let ((e79 (> e21 e18)))
(let ((e80 (distinct e23 e9)))
(let ((e81 (distinct e11 v1)))
(let ((e82 (distinct e13 e11)))
(let ((e83 (> e11 e30)))
(let ((e84 (<= e29 e23)))
(let ((e85 (>= e25 e12)))
(let ((e86 (<= e20 e16)))
(let ((e87 (distinct e13 e24)))
(let ((e88 (>= e21 e29)))
(let ((e89 (<= e24 e7)))
(let ((e90 (<= e6 e27)))
(let ((e91 (= e27 e21)))
(let ((e92 (>= e30 e28)))
(let ((e93 (> e28 e19)))
(let ((e94 (distinct e16 v1)))
(let ((e95 (= v0 e29)))
(let ((e96 (distinct e23 e13)))
(let ((e97 (<= e24 e9)))
(let ((e98 (< e15 e29)))
(let ((e99 (< e28 e24)))
(let ((e100 (= e7 e14)))
(let ((e101 (>= e25 e23)))
(let ((e102 (= e20 e23)))
(let ((e103 (distinct e12 e24)))
(let ((e104 (<= e7 e26)))
(let ((e105 (> e16 e6)))
(let ((e106 (< e20 e22)))
(let ((e107 (<= e13 e10)))
(let ((e108 (= e27 e9)))
(let ((e109 (distinct e9 e14)))
(let ((e110 (<= e10 e28)))
(let ((e111 (>= e19 v1)))
(let ((e112 (= e10 e28)))
(let ((e113 (distinct e23 e18)))
(let ((e114 (> e13 e21)))
(let ((e115 (< e16 e8)))
(let ((e116 (<= e12 e30)))
(let ((e117 (distinct e21 e23)))
(let ((e118 (distinct e26 e12)))
(let ((e119 (<= e12 e7)))
(let ((e120 (<= e6 e9)))
(let ((e121 (= e26 v1)))
(let ((e122 (>= e22 e30)))
(let ((e123 (= e24 e6)))
(let ((e124 (distinct e5 e28)))
(let ((e125 (<= e30 e20)))
(let ((e126 (distinct e12 e24)))
(let ((e127 (distinct e18 e19)))
(let ((e128 (= e24 e9)))
(let ((e129 (< e26 e9)))
(let ((e130 (>= e19 e16)))
(let ((e131 (= e27 v1)))
(let ((e132 (> e20 e7)))
(let ((e133 (= e25 e16)))
(let ((e134 (<= v1 e23)))
(let ((e135 (< v0 v1)))
(let ((e136 (<= e18 e21)))
(let ((e137 (= e25 e27)))
(let ((e138 (>= e24 e26)))
(let ((e139 (< e21 e19)))
(let ((e140 (< e16 e7)))
(let ((e141 (= e16 e18)))
(let ((e142 (< e19 v0)))
(let ((e143 (<= e19 e19)))
(let ((e144 (< e20 e7)))
(let ((e145 (<= e21 e19)))
(let ((e146 (>= e24 e28)))
(let ((e147 (distinct e24 e6)))
(let ((e148 (>= e26 e20)))
(let ((e149 (<= e12 e18)))
(let ((e150 (<= e14 e20)))
(let ((e151 (distinct e29 v0)))
(let ((e152 (< e17 e23)))
(let ((e153 (>= e14 e24)))
(let ((e154 (distinct e8 e14)))
(let ((e155 (> e18 e17)))
(let ((e156 (= e19 e30)))
(let ((e157 (distinct e14 e12)))
(let ((e158 (> e6 e26)))
(let ((e159 (distinct e6 e11)))
(let ((e160 (xor e36 e65)))
(let ((e161 (or e140 e62)))
(let ((e162 (not e132)))
(let ((e163 (and e119 e51)))
(let ((e164 (=> e92 e148)))
(let ((e165 (not e74)))
(let ((e166 (=> e137 e100)))
(let ((e167 (or e105 e138)))
(let ((e168 (=> e166 e82)))
(let ((e169 (= e55 e161)))
(let ((e170 (xor e130 e87)))
(let ((e171 (ite e50 e34 e42)))
(let ((e172 (or e78 e102)))
(let ((e173 (not e149)))
(let ((e174 (not e127)))
(let ((e175 (= e123 e95)))
(let ((e176 (ite e33 e88 e40)))
(let ((e177 (and e112 e115)))
(let ((e178 (and e104 e90)))
(let ((e179 (or e163 e175)))
(let ((e180 (and e114 e154)))
(let ((e181 (ite e98 e143 e96)))
(let ((e182 (not e46)))
(let ((e183 (=> e69 e31)))
(let ((e184 (and e179 e99)))
(let ((e185 (= e156 e174)))
(let ((e186 (ite e122 e145 e177)))
(let ((e187 (xor e76 e93)))
(let ((e188 (= e120 e79)))
(let ((e189 (or e157 e68)))
(let ((e190 (or e186 e171)))
(let ((e191 (= e73 e94)))
(let ((e192 (=> e89 e139)))
(let ((e193 (or e191 e49)))
(let ((e194 (= e70 e192)))
(let ((e195 (=> e103 e80)))
(let ((e196 (=> e113 e135)))
(let ((e197 (=> e45 e101)))
(let ((e198 (= e187 e146)))
(let ((e199 (and e193 e193)))
(let ((e200 (ite e47 e58 e129)))
(let ((e201 (or e155 e195)))
(let ((e202 (=> e43 e67)))
(let ((e203 (xor e152 e136)))
(let ((e204 (and e39 e134)))
(let ((e205 (= e198 e131)))
(let ((e206 (not e141)))
(let ((e207 (and e164 e178)))
(let ((e208 (not e142)))
(let ((e209 (not e182)))
(let ((e210 (ite e194 e72 e167)))
(let ((e211 (= e66 e160)))
(let ((e212 (and e77 e61)))
(let ((e213 (not e209)))
(let ((e214 (= e37 e184)))
(let ((e215 (=> e38 e41)))
(let ((e216 (and e165 e71)))
(let ((e217 (not e85)))
(let ((e218 (not e108)))
(let ((e219 (ite e60 e121 e159)))
(let ((e220 (=> e212 e109)))
(let ((e221 (xor e118 e200)))
(let ((e222 (or e180 e59)))
(let ((e223 (=> e172 e162)))
(let ((e224 (not e219)))
(let ((e225 (xor e44 e210)))
(let ((e226 (not e214)))
(let ((e227 (and e201 e110)))
(let ((e228 (ite e91 e226 e188)))
(let ((e229 (and e196 e32)))
(let ((e230 (and e128 e53)))
(let ((e231 (or e224 e224)))
(let ((e232 (xor e124 e197)))
(let ((e233 (=> e229 e205)))
(let ((e234 (= e106 e52)))
(let ((e235 (and e211 e173)))
(let ((e236 (and e225 e107)))
(let ((e237 (= e147 e232)))
(let ((e238 (not e111)))
(let ((e239 (not e231)))
(let ((e240 (xor e183 e189)))
(let ((e241 (=> e215 e228)))
(let ((e242 (or e239 e56)))
(let ((e243 (= e97 e208)))
(let ((e244 (xor e57 e86)))
(let ((e245 (not e133)))
(let ((e246 (= e83 e185)))
(let ((e247 (ite e216 e125 e64)))
(let ((e248 (and e117 e233)))
(let ((e249 (or e63 e221)))
(let ((e250 (ite e242 e249 e222)))
(let ((e251 (xor e204 e207)))
(let ((e252 (and e206 e220)))
(let ((e253 (and e237 e223)))
(let ((e254 (=> e48 e81)))
(let ((e255 (not e218)))
(let ((e256 (not e230)))
(let ((e257 (=> e153 e235)))
(let ((e258 (and e151 e116)))
(let ((e259 (not e150)))
(let ((e260 (and e252 e241)))
(let ((e261 (xor e213 e238)))
(let ((e262 (=> e256 e259)))
(let ((e263 (=> e248 e176)))
(let ((e264 (not e84)))
(let ((e265 (ite e199 e202 e75)))
(let ((e266 (xor e35 e190)))
(let ((e267 (xor e254 e126)))
(let ((e268 (= e261 e247)))
(let ((e269 (xor e144 e250)))
(let ((e270 (not e253)))
(let ((e271 (xor e158 e263)))
(let ((e272 (xor e270 e246)))
(let ((e273 (xor e265 e234)))
(let ((e274 (and e54 e257)))
(let ((e275 (xor e258 e267)))
(let ((e276 (ite e260 e264 e274)))
(let ((e277 (or e266 e217)))
(let ((e278 (or e168 e244)))
(let ((e279 (= e276 e245)))
(let ((e280 (and e243 e273)))
(let ((e281 (not e279)))
(let ((e282 (xor e272 e240)))
(let ((e283 (ite e181 e271 e262)))
(let ((e284 (and e236 e269)))
(let ((e285 (or e169 e283)))
(let ((e286 (=> e170 e285)))
(let ((e287 (=> e251 e281)))
(let ((e288 (or e227 e280)))
(let ((e289 (and e277 e277)))
(let ((e290 (ite e289 e278 e275)))
(let ((e291 (xor e203 e288)))
(let ((e292 (and e287 e255)))
(let ((e293 (or e284 e291)))
(let ((e294 (ite e282 e268 e282)))
(let ((e295 (=> e294 e292)))
(let ((e296 (or e290 e286)))
(let ((e297 (not e295)))
(let ((e298 (=> e297 e296)))
(let ((e299 (or e293 e293)))
(let ((e300 (not e298)))
(let ((e301 (and e300 e299)))
e301
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
